ds:x:Id fp Type, da:a:Knd fp Type. with declarations ds:dsda:da  MsgA 

latex

Definitions	Id, t  T, Knd, type List, x.A(x), x. t(x), x:A. B(x), , IdLnk, x:AB(x), Void, Type, 2of(t), rcv(l,tg), KindDeq, f(x)?z, 1of(t), Valtype(da;k), x:AB(x), State(ds), IdDeq, Prop, locl(a), mk-ma, with declarations ds:dsda:da, a:A fp B(a), MsgA
Lemmas	fpf wf, mk-ma wf, locl wf, id-deq wf, ma-state wf, ma-valtype wf, pi1 wf, fpf-cap wf, Kind-deq wf, rcv wf, pi2 wf, IdLnk wf, fpf-empty wf, Knd wf, Id wf